es:ES, i:Id, a:Atom1. i >> a  Prop 

latex

Definitions	t  T, x:A. B(x), Void, Unit, locl(a), f(a), left+right, x. t(x), type List, s = t, Id, #$n, a<b, False, P  Q, A, AB, , {x:A| B(x) }, , Atom, x:AB(x), IdLnk, state@i, Msg, S  T, vartype(i;x), S  T, Choose(i), x:T>>a, Send(i), Prop, P  Q, Trans(i), i >> a, ES, Atom$n, kindtype(i;k), x.A(x), Type, Knd, x:AB(x), AtomFree(T;x)
Lemmas	event system wf, es-trans wf, es-send wf, inheres wf, es-choose wf, es-vartype wf, es-Msg wf, atom-free-dep-function, es-state wf, atom-free-es-state, atom-free-Id, atom-free-es-Msg, Knd wf, Id wf, locl wf, unit wf, es-kindtype wf, atom-free-es-kindtype, atom-free-Knd